| Definitions | Top, tt, Y, ff, reduce(f;k;as), t.2, t.1, deq-member(eq;x;L), f(x), x : v, if b then t else f fi ,  , Normal(ds), Normal(T), P & Q,   x,y. t(x;y), x  dom(f),  b, t T, x. t(x),  , R-state(R;i),  xdom(f). v=f(x)   P(x;v), R-Feasible(R), P Q, x:A. B(x),  A, P  Q, P  Q, Unit, False, x(s1,s2), {T},  , a:A fp B(a), x(s), S  T,  |
| Lemmas | fpf-empty wf, tagof wf, fpf-cap wf, eq lnk wf, fpf-join wf, fpf-join-ap-sq, fpf-join-dom, Rrframe wf, Rbframe wf, Raframe wf, finite-prob-space wf, Rpre wf, Rsends wf, decl-type wf, decl-state wf, Reffect wf, lnk wf, ldst wf, isrcv wf, l member wf, assert-deq-member, deq-member wf, IdLnk wf, Rsframe wf, Knd wf, Rframe wf, rationals wf, Rinit wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, int inc rationals, bfalse wf, eqof wf, bor wf, assert-eq-id, eqtt to assert, iff transitivity, bool wf, eq id wf, Rplus wf, Rnone wf, true wf, false wf, es realizer wf, top wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, R-state wf, id-deq wf, Id wf, fpf-all wf, R-Feasible wf, es realizer-induction |